/*
	・ファイルを必ずどこかのディレクトリに属させる
	・ルートディレクトリはディレクトリの要素に属さない
	・循環参照させない
*/
module filesystem

// オブジェクト
abstract sig Object {}

// ディレクトリ
sig Directory extends Object { 
	contents: set Object
}{
	// サブディレクトリとしてルートディレクトリが存在することはない
	no r: Root | 
		r in contents
}

// ルートディレクトリ
one sig Root extends Directory{}

// ファイル
sig File extends Object {
}{
	// ファイルは必ずどこかのディレクトリに属する
	one d: Directory |
		this in d.contents
}

// エイリアス(リンク)
sig Alias extends File {
	to : Object
}

// ディレクトリを循環参照させない
fact NoCycleDir { 
	no d: Directory |
		d in d.^contents
}

// 全てのディレクトリ(ルートディレクトリ以外)はルートディレクトリから必ずたどれる
fact DirTraceableRoot {
	one r: Root | all d: Directory - Root |
		d in r.^contents
}

pred show{}
run show for 5
